// *.CNF generator
//$Id: generator.cpp 533 2010-07-25 12:45:06Z Oleg.Bulychov $

#include "stdafx.h"

using namespace std;

bool Sat(vector<int> const& var, vector<int> const& clause)
{
    for (size_t j = 0; j < clause.size(); ++j)
    {
        int id = clause[j];
        if (id < 0)
        {
            id = -id-1;
            if (!var[id])
                return true;
        }
        else
        {
            id -=1;
            if (var[id])
                return true;
        }
    }
    return false;
}

bool Find(vector<int> const& clause, int k)
{
    for (size_t j = 0; j < clause.size(); ++j)
    {
        if (abs(clause[j]) == abs(k))
            return true;
    }
    return false;
}

int main(int argc, char* argv[])
{
    //cout << "SAT gena" << endl;
    if (argc != 7)
    {
        cout << "usage: " << argv[0] << " randseed vars clauses min_clause_len max_clause_len allow_unsat" << endl;
        return -1;
    }
    unsigned int rand_seed = ::strtol(argv[1], NULL, 0);
    srand(rand_seed);
    int vars = ::strtol(argv[2], NULL, 0);
    int clauses = ::strtol(argv[3], NULL, 0);
    int min_clause_len = ::strtol(argv[4], NULL, 0);
    int max_clause_len = ::strtol(argv[5], NULL, 0);
    bool unsat = ::strtol(argv[6], NULL, 0) != 0;
    //cout << vars << " " << clauses << " " << min_clause_len << ".." << max_clause_len << endl;
    vector<int> var;
    var.reserve(vars);
    for (int i = 0; i < vars; ++i)
        var.push_back(0/*rand() & 1*/);
    int vars_dp = vars;
    if (!unsat)
        vars_dp -= 1;
    cout << "p cnf " << vars << " " << clauses << endl;
    for (int i = 0; i < clauses; ++i)
    {
        size_t r = 0;
        if (max_clause_len > min_clause_len)
            r = rand() % (max_clause_len - min_clause_len);
        r += min_clause_len;
        vector<int> clause;
        for(;;)
        {
            clause.clear();
            for (size_t j = 0; j < r; ++j)
            {
                for (;;)
                {
                    int k = 1 + (vars_dp ? (rand() % vars_dp) : 0);
                    if (rand() % 3 == 0)
                        k = -k;
                    if (!Find(clause, k))
                    {
                        clause.push_back(k);
                        break;
                    }
                }
            }
            if (unsat || Sat(var, clause))
                break;
            clause.push_back(vars);
            break;
        }
        for (size_t j = 0; j < clause.size(); ++j)
        {
            cout << clause[j] << " ";
        }
        cout << 0 << endl;
    }
#if (_MSC_VER > 0)
    FILE* out = stdout;
    if(!out->_ptr)
    {
        cout << "press <enter>";
        _getch();
    }
#endif
    return 0;
}

